package org.xteam.sled.semantic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

import org.xteam.sled.semantic.exp.Exp;
import org.xteam.sled.semantic.exp.IExpRewriter;


public class Constraints extends SequenceElement {
	
	private TokenClass cls;
	private Map<Field, Exp> exprs;
	private List<Constraint> constraints;
	
	public Constraints(Constraint c) {
		this(new HashMap<Field, Exp>(), new ArrayList<Constraint>());
		cls = c.field().cls();
		constraints.add(c);
	}
	
	public Constraints(Map<Field, Exp> exprs, List<Constraint> cc) {
		this.exprs = exprs;
		this.constraints = cc;
		if (cc.size() > 0)
			cls = cc.get(0).field().cls();
	}

	public Constraints(TokenClass cls, Map<Field, Exp> exprs) {
		this.cls = cls;
		this.exprs = exprs;
		this.constraints = new ArrayList<Constraint>();
	}

	public Constraints(TokenClass cls, Map<Field, Exp> exprs,
			List<Constraint> constraints) {
		this.cls = cls;
		this.exprs = exprs;
		this.constraints = constraints;
	}

	public TokenClass tokenClass() {
		return cls;
	}
	
	public boolean hasInputOrLabels() {
		return exprs.size() > 0;
	}
	
	public List<Constraint> getConstraints() {
		return constraints;
	}
	
	public boolean isContradictory() {
		for (Constraint cnst : constraints) {
			if (cnst.isContradictory()) {
				return true;
			}
		}
		return false;
	}

	public int width() {
		return cls.size();
	}
	
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		if (exprs.size() > 0)
			buffer.append(exprs.toString());
		boolean isFirst = true;
		for (Constraint cnst : constraints) {
			if (isFirst)
				isFirst = false;
			else
				buffer.append(" & ");
			buffer.append(cnst.toString());
		}
		return buffer.toString();
	}

	public Constraints merge(Constraints other) {
		if (tokenClass() != other.tokenClass()) {
			throw new RuntimeException(
					"Shapes differ for &; left sequent from class `"
							+ tokenClass().name()
							+ "'; right sequent from class `"
							+ other.tokenClass().name() + "'");
		}
		return new Constraints(cls, mergeBindings(other.exprs),
				mergeConstraints(other.constraints));
	}

	private Map<Field, Exp> mergeBindings(Map<Field, Exp> others) {
		Map<Field, Exp> result = new HashMap<Field, Exp>(exprs);
		for (Field f : others.keySet()) {
			if (result.containsKey(f))
				throw new RuntimeException("Multiple field bindings for field `" + f.name() + "'");
			result.put(f, others.get(f));
		}
		return result;
	}
	
	private List<Constraint> mergeConstraints(List<Constraint> others) {
		Map<Field, Constraint> result = new HashMap<Field, Constraint>();
		for (Constraint c : constraints) {
			if (result.containsKey(c.field())) {
				result.put(c.field(), c.intersection(result.get(c.field())));
			} else {
				result.put(c.field(), c);
			}
		}
		for (Constraint c : others) {
			if (result.containsKey(c.field())) {
				result.put(c.field(), c.intersection(result.get(c.field())));
			} else {
				result.put(c.field(), c);
			}
		}
		return new ArrayList<Constraint>(result.values());
	}

	@Override
	public SequenceElement substitutePC(int k, Exp addBitsToPC) {
		if (k == 0)
			return this;
		Map<Field, Exp> newExprs = new HashMap<Field, Exp>();
		for (Field f : exprs.keySet()) {
			newExprs.put(f, new Disjunct.PCSubstitute(addBitsToPC).rewrite(exprs.get(f)));
		}
		return new Constraints(cls, newExprs, constraints);
	}

	@Override
	public SequenceElement substitute(IExpRewriter subs) {
		Map<Field, Exp> newExprs = new HashMap<Field, Exp>();
		for (Field f : exprs.keySet()) {
			newExprs.put(f, subs.rewrite(exprs.get(f)));
		}
		return new Constraints(cls, newExprs, constraints);
	}

}
